Termination w.r.t. Q proof of /tmp/tmpMR-_j

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

Q is empty.

↳ QTRS

  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)
or(true, b) → true
or(false, b) → b

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

start(i) → busy(F, closed, stop, false, false, false, i)
busy(fl, open, up, b1, b2, b3, i) → incorrect
busy(fl, open, down, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(B, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(F, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i)) → idle(S, closed, stop, false, false, false, newbuttons(i1, i2, i3, i))
busy(B, open, stop, false, b2, b3, i) → idle(B, closed, stop, false, b2, b3, i)
busy(F, open, stop, b1, false, b3, i) → idle(F, closed, stop, b1, false, b3, i)
busy(S, open, stop, b1, b2, false, i) → idle(S, closed, stop, b1, b2, false, i)
idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) → busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)

Used ordering:
Polynomial interpretation [25]:

POL(B) = 0
POL(BF) = 0
POL(F) = 0
POL(FS) = 0
POL(S) = 0
POL(busy(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = 2·x₁ + x₂ + 2·x₃ + 2·x₄ + 2·x₅ + 2·x₆ + 2·x₇
POL(closed) = 0
POL(correct) = 0
POL(down) = 0
POL(empty) = 0
POL(false) = 0
POL(idle(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = 2·x₁ + x₂ + 2·x₃ + 2·x₄ + 2·x₅ + 2·x₆ + x₇
POL(incorrect) = 0
POL(newbuttons(x₁, x₂, x₃, x₄)) = 1 + 2·x₁ + 2·x₂ + 2·x₃ + 2·x₄
POL(open) = 2
POL(or(x₁, x₂)) = x₁ + x₂
POL(start(x₁)) = 1 + 2·x₁
POL(stop) = 0
POL(true) = 1
POL(up) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
or(true, b) → true
or(false, b) → b

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)
or(true, b) → true
or(false, b) → b

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

or(true, b) → true
or(false, b) → b

Used ordering:
Polynomial interpretation [25]:

POL(B) = 0
POL(BF) = 0
POL(F) = 0
POL(FS) = 0
POL(S) = 0
POL(busy(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = 2·x₁ + 2·x₂ + x₃ + x₄ + 2·x₅ + 2·x₆ + x₇
POL(closed) = 0
POL(correct) = 0
POL(down) = 0
POL(empty) = 0
POL(false) = 0
POL(idle(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = 2·x₁ + 2·x₂ + x₃ + x₄ + 2·x₅ + 2·x₆ + x₇
POL(incorrect) = 0
POL(open) = 0
POL(or(x₁, x₂)) = 1 + x₁ + x₂
POL(stop) = 0
POL(true) = 0
POL(up) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

busy(B, closed, stop, false, false, false, empty) → correct
busy(F, closed, stop, false, false, false, empty) → correct
busy(S, closed, stop, false, false, false, empty) → correct
busy(B, d, stop, true, b2, b3, i) → idle(B, open, stop, false, b2, b3, i)
busy(F, d, stop, b1, true, b3, i) → idle(F, open, stop, b1, false, b3, i)
busy(S, d, stop, b1, b2, true, i) → idle(S, open, stop, b1, b2, false, i)

Used ordering:
Polynomial interpretation [25]:

POL(B) = 0
POL(BF) = 0
POL(F) = 0
POL(FS) = 0
POL(S) = 0
POL(busy(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = 2·x₁ + 2·x₂ + x₃ + x₄ + x₅ + x₆ + x₇
POL(closed) = 0
POL(correct) = 2
POL(down) = 0
POL(empty) = 0
POL(false) = 1
POL(idle(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = 2·x₁ + 2·x₂ + x₃ + x₄ + x₅ + x₆ + x₇
POL(incorrect) = 0
POL(open) = 0
POL(stop) = 0
POL(true) = 2
POL(up) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect
busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

busy(BF, d, stop, b1, b2, b3, i) → incorrect
busy(FS, d, stop, b1, b2, b3, i) → incorrect

Used ordering:
Polynomial interpretation [25]:

POL(B) = 0
POL(BF) = 0
POL(F) = 0
POL(FS) = 0
POL(S) = 0
POL(busy(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = 2 + x₁ + x₂ + x₃ + x₄ + x₅ + x₆ + x₇
POL(closed) = 0
POL(down) = 0
POL(empty) = 0
POL(false) = 0
POL(idle(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = 2 + x₁ + x₂ + x₃ + x₄ + x₅ + x₆ + x₇
POL(incorrect) = 1
POL(stop) = 0
POL(true) = 0
POL(up) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

Q restricted rewrite system:
The TRS R consists of the following rules:

busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)

Q is empty.

We have applied [19,8] to switch to innermost. The TRS R 1 is none

The TRS R 2 is

busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)

The signature Sigma is {busy, idle}

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)

The set Q consists of the following terms:

busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)

The TRS R consists of the following rules:

busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)

The set Q consists of the following terms:

busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)

The TRS R consists of the following rules:

busy(B, closed, down, b1, b2, b3, i) → idle(B, closed, stop, b1, b2, b3, i)
busy(S, closed, up, b1, b2, b3, i) → idle(S, closed, stop, b1, b2, b3, i)
busy(B, closed, up, true, b2, b3, i) → idle(B, closed, stop, true, b2, b3, i)
busy(F, closed, up, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(F, closed, down, b1, true, b3, i) → idle(F, closed, stop, b1, true, b3, i)
busy(S, closed, down, b1, b2, true, i) → idle(S, closed, stop, b1, b2, true, i)
busy(B, closed, up, false, b2, b3, i) → idle(BF, closed, up, false, b2, b3, i)
busy(F, closed, up, b1, false, b3, i) → idle(FS, closed, up, b1, false, b3, i)
busy(F, closed, down, b1, false, b3, i) → idle(BF, closed, down, b1, false, b3, i)
busy(S, closed, down, b1, b2, false, i) → idle(FS, closed, down, b1, b2, false, i)
busy(BF, closed, up, b1, b2, b3, i) → idle(F, closed, up, b1, b2, b3, i)
busy(BF, closed, down, b1, b2, b3, i) → idle(B, closed, down, b1, b2, b3, i)
busy(FS, closed, up, b1, b2, b3, i) → idle(S, closed, up, b1, b2, b3, i)
busy(FS, closed, down, b1, b2, b3, i) → idle(F, closed, down, b1, b2, b3, i)
busy(B, closed, stop, false, true, b3, i) → idle(B, closed, up, false, true, b3, i)
busy(B, closed, stop, false, false, true, i) → idle(B, closed, up, false, false, true, i)
busy(F, closed, stop, true, false, b3, i) → idle(F, closed, down, true, false, b3, i)
busy(F, closed, stop, false, false, true, i) → idle(F, closed, up, false, false, true, i)
busy(S, closed, stop, b1, true, false, i) → idle(S, closed, down, b1, true, false, i)
busy(S, closed, stop, true, false, false, i) → idle(S, closed, down, true, false, false, i)
idle(fl, d, m, b1, b2, b3, empty) → busy(fl, d, m, b1, b2, b3, empty)

The set Q consists of the following terms:

busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)

R is empty.
The set Q consists of the following terms:

busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

busy(B, closed, down, x0, x1, x2, x3)
busy(S, closed, up, x0, x1, x2, x3)
busy(B, closed, up, true, x0, x1, x2)
busy(F, closed, up, x0, true, x1, x2)
busy(F, closed, down, x0, true, x1, x2)
busy(S, closed, down, x0, x1, true, x2)
busy(B, closed, up, false, x0, x1, x2)
busy(F, closed, up, x0, false, x1, x2)
busy(F, closed, down, x0, false, x1, x2)
busy(S, closed, down, x0, x1, false, x2)
busy(BF, closed, up, x0, x1, x2, x3)
busy(BF, closed, down, x0, x1, x2, x3)
busy(FS, closed, up, x0, x1, x2, x3)
busy(FS, closed, down, x0, x1, x2, x3)
busy(B, closed, stop, false, true, x0, x1)
busy(B, closed, stop, false, false, true, x0)
busy(F, closed, stop, true, false, x0, x1)
busy(F, closed, stop, false, false, true, x0)
busy(S, closed, stop, x0, true, false, x1)
busy(S, closed, stop, true, false, false, x0)
idle(x0, x1, x2, x3, x4, x5, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i)
BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule BUSY(B, closed, stop, false, false, true, i) → IDLE(B, closed, up, false, false, true, i) we obtained the following new rules:

BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule BUSY(B, closed, up, false, b2, b3, i) → IDLE(BF, closed, up, false, b2, b3, i) we obtained the following new rules:

BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule BUSY(F, closed, up, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i) we obtained the following new rules:

BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i)
BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule BUSY(FS, closed, up, b1, b2, b3, i) → IDLE(S, closed, up, b1, b2, b3, i) we obtained the following new rules:

BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule BUSY(FS, closed, down, b1, b2, b3, i) → IDLE(F, closed, down, b1, b2, b3, i) we obtained the following new rules:

BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule BUSY(S, closed, down, b1, b2, false, i) → IDLE(FS, closed, down, b1, b2, false, i) we obtained the following new rules:

BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule BUSY(BF, closed, up, b1, b2, b3, i) → IDLE(F, closed, up, b1, b2, b3, i) we obtained the following new rules:

BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule BUSY(F, closed, down, b1, true, b3, i) → IDLE(F, closed, stop, b1, true, b3, i) we obtained the following new rules:

BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule BUSY(S, closed, stop, b1, true, false, i) → IDLE(S, closed, down, b1, true, false, i) we obtained the following new rules:

BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule BUSY(S, closed, down, b1, b2, true, i) → IDLE(S, closed, stop, b1, b2, true, i) we obtained the following new rules:

BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule BUSY(B, closed, up, true, b2, b3, i) → IDLE(B, closed, stop, true, b2, b3, i) we obtained the following new rules:

BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule IDLE(fl, d, m, b1, b2, b3, empty) → BUSY(fl, d, m, b1, b2, b3, empty) we obtained the following new rules:

IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
IDLE(S, closed, stop, z0, z1, true, empty) → BUSY(S, closed, stop, z0, z1, true, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(F, closed, stop, z0, true, z1, empty) → BUSY(F, closed, stop, z0, true, z1, empty)
IDLE(B, closed, stop, true, z0, z1, empty) → BUSY(B, closed, stop, true, z0, z1, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
IDLE(BF, closed, up, false, z0, z1, empty) → BUSY(BF, closed, up, false, z0, z1, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(B, closed, up, true, z4, z5, empty) → IDLE(B, closed, stop, true, z4, z5, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(S, closed, stop, z0, z1, true, empty) → BUSY(S, closed, stop, z0, z1, true, empty)
IDLE(F, closed, stop, z0, true, z1, empty) → BUSY(F, closed, stop, z0, true, z1, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(F, closed, up, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(F, closed, stop, true, false, b3, i) → IDLE(F, closed, down, true, false, b3, i)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(F, closed, down, z3, true, z5, empty) → IDLE(F, closed, stop, z3, true, z5, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(S, closed, down, z3, z4, true, empty) → IDLE(S, closed, stop, z3, z4, true, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, stop, true, z0, z1, empty) → BUSY(B, closed, stop, true, z0, z1, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, stop, false, false, true, i) → IDLE(F, closed, up, false, false, true, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
IDLE(BF, closed, up, false, z0, z1, empty) → BUSY(BF, closed, up, false, z0, z1, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 9 less nodes.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
IDLE(BF, closed, up, false, z0, z1, empty) → BUSY(BF, closed, up, false, z0, z1, empty)
BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule BUSY(B, closed, up, false, z4, z5, empty) → IDLE(BF, closed, up, false, z4, z5, empty) we obtained the following new rules:

BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ Instantiation

                                                                                        ↳ QDP

                                                                                          ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
IDLE(BF, closed, up, false, z0, z1, empty) → BUSY(BF, closed, up, false, z0, z1, empty)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule IDLE(BF, closed, up, false, z0, z1, empty) → BUSY(BF, closed, up, false, z0, z1, empty) we obtained the following new rules:

IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
IDLE(BF, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ Instantiation

                                                                                        ↳ QDP

                                                                                          ↳ Instantiation

                                                                                            ↳ QDP

                                                                                              ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty)
BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
IDLE(BF, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule BUSY(BF, closed, up, z3, z4, z5, empty) → IDLE(F, closed, up, z3, z4, z5, empty) we obtained the following new rules:

BUSY(BF, closed, up, false, true, z0, empty) → IDLE(F, closed, up, false, true, z0, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ Instantiation

                                                                                        ↳ QDP

                                                                                          ↳ Instantiation

                                                                                            ↳ QDP

                                                                                              ↳ Instantiation

                                                                                                ↳ QDP

                                                                                                  ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
BUSY(BF, closed, up, false, true, z0, empty) → IDLE(F, closed, up, false, true, z0, empty)
IDLE(BF, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule BUSY(F, closed, up, b1, false, b3, i) → IDLE(FS, closed, up, b1, false, b3, i) we obtained the following new rules:

BUSY(F, closed, up, z0, false, z2, empty) → IDLE(FS, closed, up, z0, false, z2, empty)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ Instantiation

                                                                                        ↳ QDP

                                                                                          ↳ Instantiation

                                                                                            ↳ QDP

                                                                                              ↳ Instantiation

                                                                                                ↳ QDP

                                                                                                  ↳ Instantiation

                                                                                                    ↳ QDP

                                                                                                      ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
BUSY(BF, closed, up, false, true, z0, empty) → IDLE(F, closed, up, false, true, z0, empty)
IDLE(BF, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(F, closed, up, z0, false, z2, empty) → IDLE(FS, closed, up, z0, false, z2, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule BUSY(FS, closed, up, z3, z4, z5, empty) → IDLE(S, closed, up, z3, z4, z5, empty) we obtained the following new rules:

BUSY(FS, closed, up, z0, false, z1, empty) → IDLE(S, closed, up, z0, false, z1, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ Instantiation

                                                                                        ↳ QDP

                                                                                          ↳ Instantiation

                                                                                            ↳ QDP

                                                                                              ↳ Instantiation

                                                                                                ↳ QDP

                                                                                                  ↳ Instantiation

                                                                                                    ↳ QDP

                                                                                                      ↳ Instantiation

                                                                                                        ↳ QDP

                                                                                                          ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
BUSY(FS, closed, up, z0, false, z1, empty) → IDLE(S, closed, up, z0, false, z1, empty)
BUSY(BF, closed, up, false, true, z0, empty) → IDLE(F, closed, up, false, true, z0, empty)
IDLE(BF, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(F, closed, up, z0, false, z2, empty) → IDLE(FS, closed, up, z0, false, z2, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule IDLE(S, closed, up, z0, z1, z2, empty) → BUSY(S, closed, up, z0, z1, z2, empty) we obtained the following new rules:

IDLE(S, closed, up, z0, false, z1, empty) → BUSY(S, closed, up, z0, false, z1, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ Instantiation

                                                                                        ↳ QDP

                                                                                          ↳ Instantiation

                                                                                            ↳ QDP

                                                                                              ↳ Instantiation

                                                                                                ↳ QDP

                                                                                                  ↳ Instantiation

                                                                                                    ↳ QDP

                                                                                                      ↳ Instantiation

                                                                                                        ↳ QDP

                                                                                                          ↳ Instantiation

                                                                                                            ↳ QDP

                                                                                                              ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
BUSY(FS, closed, up, z0, false, z1, empty) → IDLE(S, closed, up, z0, false, z1, empty)
BUSY(BF, closed, up, false, true, z0, empty) → IDLE(F, closed, up, false, true, z0, empty)
IDLE(BF, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(F, closed, up, z0, false, z2, empty) → IDLE(FS, closed, up, z0, false, z2, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(S, closed, up, z0, false, z1, empty) → BUSY(S, closed, up, z0, false, z1, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule BUSY(S, closed, up, b1, b2, b3, i) → IDLE(S, closed, stop, b1, b2, b3, i) we obtained the following new rules:

BUSY(S, closed, up, z0, false, z1, empty) → IDLE(S, closed, stop, z0, false, z1, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ Instantiation

                                                                                        ↳ QDP

                                                                                          ↳ Instantiation

                                                                                            ↳ QDP

                                                                                              ↳ Instantiation

                                                                                                ↳ QDP

                                                                                                  ↳ Instantiation

                                                                                                    ↳ QDP

                                                                                                      ↳ Instantiation

                                                                                                        ↳ QDP

                                                                                                          ↳ Instantiation

                                                                                                            ↳ QDP

                                                                                                              ↳ Instantiation

                                                                                                                ↳ QDP

                                                                                                                  ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
BUSY(FS, closed, up, z0, false, z1, empty) → IDLE(S, closed, up, z0, false, z1, empty)
BUSY(BF, closed, up, false, true, z0, empty) → IDLE(F, closed, up, false, true, z0, empty)
IDLE(BF, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(F, closed, up, z0, false, z2, empty) → IDLE(FS, closed, up, z0, false, z2, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(S, closed, up, z0, false, z1, empty) → IDLE(S, closed, stop, z0, false, z1, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(S, closed, up, z0, false, z1, empty) → BUSY(S, closed, up, z0, false, z1, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule IDLE(S, closed, stop, z0, z1, z2, empty) → BUSY(S, closed, stop, z0, z1, z2, empty) we obtained the following new rules:

IDLE(S, closed, stop, z0, false, z1, empty) → BUSY(S, closed, stop, z0, false, z1, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ Instantiation

                                                                                        ↳ QDP

                                                                                          ↳ Instantiation

                                                                                            ↳ QDP

                                                                                              ↳ Instantiation

                                                                                                ↳ QDP

                                                                                                  ↳ Instantiation

                                                                                                    ↳ QDP

                                                                                                      ↳ Instantiation

                                                                                                        ↳ QDP

                                                                                                          ↳ Instantiation

                                                                                                            ↳ QDP

                                                                                                              ↳ Instantiation

                                                                                                                ↳ QDP

                                                                                                                  ↳ Instantiation

                                                                                                                    ↳ QDP

                                                                                                                      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

BUSY(S, closed, stop, z3, true, false, empty) → IDLE(S, closed, down, z3, true, false, empty)
BUSY(FS, closed, up, z0, false, z1, empty) → IDLE(S, closed, up, z0, false, z1, empty)
BUSY(BF, closed, up, false, true, z0, empty) → IDLE(F, closed, up, false, true, z0, empty)
IDLE(BF, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(F, closed, up, z0, false, z2, empty) → IDLE(FS, closed, up, z0, false, z2, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, up, z0, false, z1, empty) → IDLE(S, closed, stop, z0, false, z1, empty)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(S, closed, up, z0, false, z1, empty) → BUSY(S, closed, up, z0, false, z1, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(S, closed, stop, z0, false, z1, empty) → BUSY(S, closed, stop, z0, false, z1, empty)
IDLE(S, closed, down, z0, true, false, empty) → BUSY(S, closed, down, z0, true, false, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ Instantiation

                                                                                        ↳ QDP

                                                                                          ↳ Instantiation

                                                                                            ↳ QDP

                                                                                              ↳ Instantiation

                                                                                                ↳ QDP

                                                                                                  ↳ Instantiation

                                                                                                    ↳ QDP

                                                                                                      ↳ Instantiation

                                                                                                        ↳ QDP

                                                                                                          ↳ Instantiation

                                                                                                            ↳ QDP

                                                                                                              ↳ Instantiation

                                                                                                                ↳ QDP

                                                                                                                  ↳ Instantiation

                                                                                                                    ↳ QDP

                                                                                                                      ↳ DependencyGraphProof

                                                                                                                        ↳ QDP

                                                                                                                          ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(FS, closed, up, z0, false, z1, empty) → IDLE(S, closed, up, z0, false, z1, empty)
BUSY(BF, closed, up, false, true, z0, empty) → IDLE(F, closed, up, false, true, z0, empty)
IDLE(BF, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(F, closed, up, z0, false, z2, empty) → IDLE(FS, closed, up, z0, false, z2, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(S, closed, up, z0, false, z1, empty) → IDLE(S, closed, stop, z0, false, z1, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(S, closed, up, z0, false, z1, empty) → BUSY(S, closed, up, z0, false, z1, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty)
IDLE(S, closed, stop, z0, false, z1, empty) → BUSY(S, closed, stop, z0, false, z1, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule IDLE(F, closed, up, z0, z1, z2, empty) → BUSY(F, closed, up, z0, z1, z2, empty) we obtained the following new rules:

IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(F, closed, up, false, true, z0, empty) → BUSY(F, closed, up, false, true, z0, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ Instantiation

                                                                                        ↳ QDP

                                                                                          ↳ Instantiation

                                                                                            ↳ QDP

                                                                                              ↳ Instantiation

                                                                                                ↳ QDP

                                                                                                  ↳ Instantiation

                                                                                                    ↳ QDP

                                                                                                      ↳ Instantiation

                                                                                                        ↳ QDP

                                                                                                          ↳ Instantiation

                                                                                                            ↳ QDP

                                                                                                              ↳ Instantiation

                                                                                                                ↳ QDP

                                                                                                                  ↳ Instantiation

                                                                                                                    ↳ QDP

                                                                                                                      ↳ DependencyGraphProof

                                                                                                                        ↳ QDP

                                                                                                                          ↳ Instantiation

                                                                                                                            ↳ QDP

                                                                                                                              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

BUSY(FS, closed, up, z0, false, z1, empty) → IDLE(S, closed, up, z0, false, z1, empty)
BUSY(BF, closed, up, false, true, z0, empty) → IDLE(F, closed, up, false, true, z0, empty)
IDLE(BF, closed, up, false, true, z0, empty) → BUSY(BF, closed, up, false, true, z0, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
BUSY(B, closed, up, false, true, z0, empty) → IDLE(BF, closed, up, false, true, z0, empty)
BUSY(F, closed, up, z0, false, z2, empty) → IDLE(FS, closed, up, z0, false, z2, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, up, z0, false, z1, empty) → IDLE(S, closed, stop, z0, false, z1, empty)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
IDLE(F, closed, up, false, true, z0, empty) → BUSY(F, closed, up, false, true, z0, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(S, closed, up, z0, false, z1, empty) → BUSY(S, closed, up, z0, false, z1, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(S, closed, stop, z0, false, z1, empty) → BUSY(S, closed, stop, z0, false, z1, empty)
IDLE(B, closed, up, false, true, z0, empty) → BUSY(B, closed, up, false, true, z0, empty)
BUSY(B, closed, stop, false, true, b3, i) → IDLE(B, closed, up, false, true, b3, i)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 6 less nodes.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ Instantiation

                                                                                        ↳ QDP

                                                                                          ↳ Instantiation

                                                                                            ↳ QDP

                                                                                              ↳ Instantiation

                                                                                                ↳ QDP

                                                                                                  ↳ Instantiation

                                                                                                    ↳ QDP

                                                                                                      ↳ Instantiation

                                                                                                        ↳ QDP

                                                                                                          ↳ Instantiation

                                                                                                            ↳ QDP

                                                                                                              ↳ Instantiation

                                                                                                                ↳ QDP

                                                                                                                  ↳ Instantiation

                                                                                                                    ↳ QDP

                                                                                                                      ↳ DependencyGraphProof

                                                                                                                        ↳ QDP

                                                                                                                          ↳ Instantiation

                                                                                                                            ↳ QDP

                                                                                                                              ↳ DependencyGraphProof

                                                                                                                                ↳ QDP

                                                                                                                                  ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(FS, closed, up, z0, false, z1, empty) → IDLE(S, closed, up, z0, false, z1, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(F, closed, up, z0, false, z2, empty) → IDLE(FS, closed, up, z0, false, z2, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(S, closed, up, z0, false, z1, empty) → IDLE(S, closed, stop, z0, false, z1, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(S, closed, up, z0, false, z1, empty) → BUSY(S, closed, up, z0, false, z1, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(S, closed, stop, z0, false, z1, empty) → BUSY(S, closed, stop, z0, false, z1, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule BUSY(F, closed, up, z0, false, z2, empty) → IDLE(FS, closed, up, z0, false, z2, empty) we obtained the following new rules:

BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ Instantiation

                                                                                        ↳ QDP

                                                                                          ↳ Instantiation

                                                                                            ↳ QDP

                                                                                              ↳ Instantiation

                                                                                                ↳ QDP

                                                                                                  ↳ Instantiation

                                                                                                    ↳ QDP

                                                                                                      ↳ Instantiation

                                                                                                        ↳ QDP

                                                                                                          ↳ Instantiation

                                                                                                            ↳ QDP

                                                                                                              ↳ Instantiation

                                                                                                                ↳ QDP

                                                                                                                  ↳ Instantiation

                                                                                                                    ↳ QDP

                                                                                                                      ↳ DependencyGraphProof

                                                                                                                        ↳ QDP

                                                                                                                          ↳ Instantiation

                                                                                                                            ↳ QDP

                                                                                                                              ↳ DependencyGraphProof

                                                                                                                                ↳ QDP

                                                                                                                                  ↳ Instantiation

                                                                                                                                    ↳ QDP

                                                                                                                                      ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(FS, closed, up, z0, false, z1, empty) → IDLE(S, closed, up, z0, false, z1, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, up, z0, false, z1, empty) → IDLE(S, closed, stop, z0, false, z1, empty)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(S, closed, up, z0, false, z1, empty) → BUSY(S, closed, up, z0, false, z1, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(S, closed, stop, z0, false, z1, empty) → BUSY(S, closed, stop, z0, false, z1, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule IDLE(FS, closed, up, z0, false, z1, empty) → BUSY(FS, closed, up, z0, false, z1, empty) we obtained the following new rules:

IDLE(FS, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ Instantiation

                                                                                        ↳ QDP

                                                                                          ↳ Instantiation

                                                                                            ↳ QDP

                                                                                              ↳ Instantiation

                                                                                                ↳ QDP

                                                                                                  ↳ Instantiation

                                                                                                    ↳ QDP

                                                                                                      ↳ Instantiation

                                                                                                        ↳ QDP

                                                                                                          ↳ Instantiation

                                                                                                            ↳ QDP

                                                                                                              ↳ Instantiation

                                                                                                                ↳ QDP

                                                                                                                  ↳ Instantiation

                                                                                                                    ↳ QDP

                                                                                                                      ↳ DependencyGraphProof

                                                                                                                        ↳ QDP

                                                                                                                          ↳ Instantiation

                                                                                                                            ↳ QDP

                                                                                                                              ↳ DependencyGraphProof

                                                                                                                                ↳ QDP

                                                                                                                                  ↳ Instantiation

                                                                                                                                    ↳ QDP

                                                                                                                                      ↳ Instantiation

                                                                                                                                        ↳ QDP

                                                                                                                                          ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(FS, closed, up, z0, false, z1, empty) → IDLE(S, closed, up, z0, false, z1, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, up, z0, false, z1, empty) → IDLE(S, closed, stop, z0, false, z1, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(FS, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(S, closed, up, z0, false, z1, empty) → BUSY(S, closed, up, z0, false, z1, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(S, closed, stop, z0, false, z1, empty) → BUSY(S, closed, stop, z0, false, z1, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule BUSY(FS, closed, up, z0, false, z1, empty) → IDLE(S, closed, up, z0, false, z1, empty) we obtained the following new rules:

BUSY(FS, closed, up, false, false, true, empty) → IDLE(S, closed, up, false, false, true, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ Instantiation

                                                                                        ↳ QDP

                                                                                          ↳ Instantiation

                                                                                            ↳ QDP

                                                                                              ↳ Instantiation

                                                                                                ↳ QDP

                                                                                                  ↳ Instantiation

                                                                                                    ↳ QDP

                                                                                                      ↳ Instantiation

                                                                                                        ↳ QDP

                                                                                                          ↳ Instantiation

                                                                                                            ↳ QDP

                                                                                                              ↳ Instantiation

                                                                                                                ↳ QDP

                                                                                                                  ↳ Instantiation

                                                                                                                    ↳ QDP

                                                                                                                      ↳ DependencyGraphProof

                                                                                                                        ↳ QDP

                                                                                                                          ↳ Instantiation

                                                                                                                            ↳ QDP

                                                                                                                              ↳ DependencyGraphProof

                                                                                                                                ↳ QDP

                                                                                                                                  ↳ Instantiation

                                                                                                                                    ↳ QDP

                                                                                                                                      ↳ Instantiation

                                                                                                                                        ↳ QDP

                                                                                                                                          ↳ Instantiation

                                                                                                                                            ↳ QDP

                                                                                                                                              ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(FS, closed, up, false, false, true, empty) → IDLE(S, closed, up, false, false, true, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, up, z0, false, z1, empty) → IDLE(S, closed, stop, z0, false, z1, empty)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(FS, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(S, closed, up, z0, false, z1, empty) → BUSY(S, closed, up, z0, false, z1, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(S, closed, stop, z0, false, z1, empty) → BUSY(S, closed, stop, z0, false, z1, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule IDLE(S, closed, up, z0, false, z1, empty) → BUSY(S, closed, up, z0, false, z1, empty) we obtained the following new rules:

IDLE(S, closed, up, false, false, true, empty) → BUSY(S, closed, up, false, false, true, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ Instantiation

                                                                                        ↳ QDP

                                                                                          ↳ Instantiation

                                                                                            ↳ QDP

                                                                                              ↳ Instantiation

                                                                                                ↳ QDP

                                                                                                  ↳ Instantiation

                                                                                                    ↳ QDP

                                                                                                      ↳ Instantiation

                                                                                                        ↳ QDP

                                                                                                          ↳ Instantiation

                                                                                                            ↳ QDP

                                                                                                              ↳ Instantiation

                                                                                                                ↳ QDP

                                                                                                                  ↳ Instantiation

                                                                                                                    ↳ QDP

                                                                                                                      ↳ DependencyGraphProof

                                                                                                                        ↳ QDP

                                                                                                                          ↳ Instantiation

                                                                                                                            ↳ QDP

                                                                                                                              ↳ DependencyGraphProof

                                                                                                                                ↳ QDP

                                                                                                                                  ↳ Instantiation

                                                                                                                                    ↳ QDP

                                                                                                                                      ↳ Instantiation

                                                                                                                                        ↳ QDP

                                                                                                                                          ↳ Instantiation

                                                                                                                                            ↳ QDP

                                                                                                                                              ↳ Instantiation

                                                                                                                                                ↳ QDP

                                                                                                                                                  ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(FS, closed, up, false, false, true, empty) → IDLE(S, closed, up, false, false, true, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
BUSY(S, closed, up, z0, false, z1, empty) → IDLE(S, closed, stop, z0, false, z1, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(FS, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(S, closed, up, false, false, true, empty) → BUSY(S, closed, up, false, false, true, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(S, closed, stop, z0, false, z1, empty) → BUSY(S, closed, stop, z0, false, z1, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule BUSY(S, closed, up, z0, false, z1, empty) → IDLE(S, closed, stop, z0, false, z1, empty) we obtained the following new rules:

BUSY(S, closed, up, false, false, true, empty) → IDLE(S, closed, stop, false, false, true, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ Instantiation

                                                                                        ↳ QDP

                                                                                          ↳ Instantiation

                                                                                            ↳ QDP

                                                                                              ↳ Instantiation

                                                                                                ↳ QDP

                                                                                                  ↳ Instantiation

                                                                                                    ↳ QDP

                                                                                                      ↳ Instantiation

                                                                                                        ↳ QDP

                                                                                                          ↳ Instantiation

                                                                                                            ↳ QDP

                                                                                                              ↳ Instantiation

                                                                                                                ↳ QDP

                                                                                                                  ↳ Instantiation

                                                                                                                    ↳ QDP

                                                                                                                      ↳ DependencyGraphProof

                                                                                                                        ↳ QDP

                                                                                                                          ↳ Instantiation

                                                                                                                            ↳ QDP

                                                                                                                              ↳ DependencyGraphProof

                                                                                                                                ↳ QDP

                                                                                                                                  ↳ Instantiation

                                                                                                                                    ↳ QDP

                                                                                                                                      ↳ Instantiation

                                                                                                                                        ↳ QDP

                                                                                                                                          ↳ Instantiation

                                                                                                                                            ↳ QDP

                                                                                                                                              ↳ Instantiation

                                                                                                                                                ↳ QDP

                                                                                                                                                  ↳ Instantiation

                                                                                                                                                    ↳ QDP

                                                                                                                                                      ↳ Instantiation

Q DP problem:
The TRS P consists of the following rules:

BUSY(FS, closed, up, false, false, true, empty) → IDLE(S, closed, up, false, false, true, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(S, closed, up, false, false, true, empty) → IDLE(S, closed, stop, false, false, true, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(FS, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(S, closed, up, false, false, true, empty) → BUSY(S, closed, up, false, false, true, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
IDLE(S, closed, stop, z0, false, z1, empty) → BUSY(S, closed, stop, z0, false, z1, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By instantiating [15] the rule IDLE(S, closed, stop, z0, false, z1, empty) → BUSY(S, closed, stop, z0, false, z1, empty) we obtained the following new rules:

IDLE(S, closed, stop, false, false, true, empty) → BUSY(S, closed, stop, false, false, true, empty)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ AAECC Innermost

                    ↳ QTRS

                      ↳ DependencyPairsProof

                        ↳ QDP

                          ↳ UsableRulesProof

                            ↳ QDP

                              ↳ QReductionProof

                                ↳ QDP

                                  ↳ Instantiation

                                    ↳ QDP

                                      ↳ Instantiation

                                        ↳ QDP

                                          ↳ Instantiation

                                            ↳ QDP

                                              ↳ Instantiation

                                                ↳ QDP

                                                  ↳ Instantiation

                                                    ↳ QDP

                                                      ↳ Instantiation

                                                        ↳ QDP

                                                          ↳ Instantiation

                                                            ↳ QDP

                                                              ↳ Instantiation

                                                                ↳ QDP

                                                                  ↳ Instantiation

                                                                    ↳ QDP

                                                                      ↳ Instantiation

                                                                        ↳ QDP

                                                                          ↳ Instantiation

                                                                            ↳ QDP

                                                                              ↳ Instantiation

                                                                                ↳ QDP

                                                                                  ↳ DependencyGraphProof

                                                                                    ↳ QDP

                                                                                      ↳ Instantiation

                                                                                        ↳ QDP

                                                                                          ↳ Instantiation

                                                                                            ↳ QDP

                                                                                              ↳ Instantiation

                                                                                                ↳ QDP

                                                                                                  ↳ Instantiation

                                                                                                    ↳ QDP

                                                                                                      ↳ Instantiation

                                                                                                        ↳ QDP

                                                                                                          ↳ Instantiation

                                                                                                            ↳ QDP

                                                                                                              ↳ Instantiation

                                                                                                                ↳ QDP

                                                                                                                  ↳ Instantiation

                                                                                                                    ↳ QDP

                                                                                                                      ↳ DependencyGraphProof

                                                                                                                        ↳ QDP

                                                                                                                          ↳ Instantiation

                                                                                                                            ↳ QDP

                                                                                                                              ↳ DependencyGraphProof

                                                                                                                                ↳ QDP

                                                                                                                                  ↳ Instantiation

                                                                                                                                    ↳ QDP

                                                                                                                                      ↳ Instantiation

                                                                                                                                        ↳ QDP

                                                                                                                                          ↳ Instantiation

                                                                                                                                            ↳ QDP

                                                                                                                                              ↳ Instantiation

                                                                                                                                                ↳ QDP

                                                                                                                                                  ↳ Instantiation

                                                                                                                                                    ↳ QDP

                                                                                                                                                      ↳ Instantiation

                                                                                                                                                        ↳ QDP

                                                                                                                                                          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

BUSY(FS, closed, up, false, false, true, empty) → IDLE(S, closed, up, false, false, true, empty)
IDLE(BF, closed, down, z0, false, z1, empty) → BUSY(BF, closed, down, z0, false, z1, empty)
IDLE(S, closed, down, true, false, false, empty) → BUSY(S, closed, down, true, false, false, empty)
BUSY(S, closed, up, false, false, true, empty) → IDLE(S, closed, stop, false, false, true, empty)
IDLE(BF, closed, up, false, false, true, empty) → BUSY(BF, closed, up, false, false, true, empty)
IDLE(B, closed, stop, z0, z1, z2, empty) → BUSY(B, closed, stop, z0, z1, z2, empty)
BUSY(B, closed, down, b1, b2, b3, i) → IDLE(B, closed, stop, b1, b2, b3, i)
BUSY(S, closed, stop, true, false, false, i) → IDLE(S, closed, down, true, false, false, i)
IDLE(S, closed, stop, false, false, true, empty) → BUSY(S, closed, stop, false, false, true, empty)
IDLE(FS, closed, up, false, false, true, empty) → BUSY(FS, closed, up, false, false, true, empty)
BUSY(BF, closed, up, false, false, true, empty) → IDLE(F, closed, up, false, false, true, empty)
BUSY(BF, closed, down, b1, b2, b3, i) → IDLE(B, closed, down, b1, b2, b3, i)
BUSY(B, closed, up, false, false, true, empty) → IDLE(BF, closed, up, false, false, true, empty)
IDLE(F, closed, down, z0, z1, z2, empty) → BUSY(F, closed, down, z0, z1, z2, empty)
IDLE(FS, closed, down, z0, z1, false, empty) → BUSY(FS, closed, down, z0, z1, false, empty)
IDLE(S, closed, up, false, false, true, empty) → BUSY(S, closed, up, false, false, true, empty)
IDLE(F, closed, down, true, false, z0, empty) → BUSY(F, closed, down, true, false, z0, empty)
BUSY(B, closed, stop, false, false, true, empty) → IDLE(B, closed, up, false, false, true, empty)
BUSY(S, closed, down, z3, z4, false, empty) → IDLE(FS, closed, down, z3, z4, false, empty)
IDLE(F, closed, up, false, false, true, empty) → BUSY(F, closed, up, false, false, true, empty)
IDLE(B, closed, down, z0, z1, z2, empty) → BUSY(B, closed, down, z0, z1, z2, empty)
IDLE(B, closed, up, false, false, true, empty) → BUSY(B, closed, up, false, false, true, empty)
BUSY(F, closed, down, b1, false, b3, i) → IDLE(BF, closed, down, b1, false, b3, i)
BUSY(F, closed, up, false, false, true, empty) → IDLE(FS, closed, up, false, false, true, empty)
BUSY(FS, closed, down, z3, z4, z5, empty) → IDLE(F, closed, down, z3, z4, z5, empty)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 25 less nodes.